Nuprl Lemma : interleaved_family_wf
4,23
postcript
pdf
T
,
I
:Type,
L
:(
I
(
T
List)),
L2
:
T
List. interleaved_family(
T
;
I
;
L
;
L2
)
Prop
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
interleaved_family_occurence(
T
;
I
;
L
;
L2
;
f
)
,
||
as
||
,
{
i
..
j
}
,
Prop
,
x
:
A
.
B
(
x
)
,
interleaved_family(
T
;
I
;
L
;
L2
)
Lemmas
int
seg
wf
,
length
wf1
,
interleaved
family
occurence
wf
origin
T, I:Type, L:(I
(T List)), L2:T List. interleaved_family(T;I;L;L2) 
Prop T, I:Type, L:(I(T List)), L2:T List. interleaved_family(T;I;L;L2) Prop Tx:A. B(x)
}
x:A. B(x)